Introduction in [Giesl and Middeldorp - RPC'01]

Summary: ExIntrod_GM01

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation
  2. Zantema's transformation
  3. Ferreira and Ribeiro's transformation
• Positive results:
  1. Giesl and Middeldorp's transformation (AProVE)
  2. CSRPO
  3. CSDPs
  4. Polynomial interpretation (MuTerm)

CS-TRS ExIntrod_GM01 (file ExIntrod_GM01.csr)

Functions:  incr nil cons s adx nats zeros 0 head tail

Constructors:  nil cons s 0

Variables:  X L

Arities: 

ar(incr) = 1
ar(nil) = 0
ar(cons) = 2
ar(s) = 1
ar(adx) = 1
ar(nats) = 0
ar(zeros) = 0
ar(0) = 0
ar(head) = 1
ar(tail) = 1

Replacement map: 

µ(incr)={1}
µ(nil)={}
µ(cons)={1}
µ(s)={1}
µ(adx)={1}
µ(nats)={}
µ(zeros)={}
µ(0)={}
µ(head)={1}
µ(tail)={1}

Rules:   (file ExIntrod_GM01)   

incr(nil) -> nil
incr(cons(X,L)) -> cons(s(X),incr(L))
adx(nil) -> nil
adx(cons(X,L)) -> incr(cons(X,adx(L)))
nats -> adx(zeros)
zeros -> cons(0,zeros)
head(cons(X,L)) -> X
tail(cons(X,L)) -> L

The CS-TRS in OBJ format (file ExIntrod_GM01.obj):

obj ExIntrod_GM01 is
  sort S .
  op incr : S -> S .
  op nil : -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op adx : S -> S .
  op nats : -> S .
  op zeros : -> S .
  op 0 : -> S .
  op head : S -> S .
  op tail : S -> S .
  vars X L : S .
  eq incr(nil) = nil .
  eq incr(cons(X,L)) = cons(s(X),incr(L)) .
  eq adx(nil) = nil .
  eq adx(cons(X,L)) = incr(cons(X,adx(L))) .
  eq nats = adx(zeros) .
  eq zeros = cons(0,zeros) .
  eq head(cons(X,L)) = X .
  eq tail(cons(X,L)) = L .
endo

Negative results

1. The µ-termination of ExIntrod_GM01 cannot be proved terminating by using Lucas' transformation. The TRS ExIntrod_GM01_L:

       incr(nil) -> nil
       incr(cons(X)) -> cons(s(X))
       adx(nil) -> nil
       adx(cons(X)) -> incr(cons(X))
       nats -> adx(zeros)
       zeros -> cons(0)
       head(cons(X)) -> X
       tail(cons(X)) -> L
       

   contains extra variables.
2. The µ-termination of ExIntrod_GM01 cannot be proved terminating by using Zantema's transformation. The TRS ExIntrod_GM01_Z:

       incr(nil) -> nil
       incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
       adx(nil) -> nil
       adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
       nats -> adx(zeros)
       zeros -> cons(0,n__zeros)
       head(cons(X,L)) -> X
       tail(cons(X,L)) -> activate(L)
       incr(X) -> n__incr(X)
       adx(X) -> n__adx(X)
       zeros -> n__zeros
       activate(n__incr(X)) -> incr(X)
       activate(n__adx(X)) -> adx(X)
       activate(n__zeros) -> zeros
       activate(X) -> X
       

   is not terminating (see [GM04]).
3. The µ-termination of ExIntrod_GM01 cannot be proved terminating by using Ferreira and Ribeiro's transformation. The TRS ExIntrod_GM01_FR:

       incr(nil) -> nil
       incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
       adx(nil) -> nil
       adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
       nats -> adx(zeros)
       zeros -> cons(0,n__zeros)
       head(cons(X,L)) -> X
       tail(cons(X,L)) -> activate(L)
       incr(X) -> n__incr(X)
       adx(X) -> n__adx(X)
       zeros -> n__zeros
       activate(n__incr(X)) -> incr(activate(X))
       activate(n__adx(X)) -> adx(activate(X))
       activate(n__zeros) -> zeros
       activate(X) -> X
       

   is not terminating (see [GM04]).

Positive results

1. The µ-termination of ExIntrod_GM01 can be proved by using Giesl and Middeldorp's transformation. The TRS ExIntrod_GM01_GM:

      a__incr(nil) -> nil
      a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
      a__adx(nil) -> nil
      a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
      a__nats -> a__adx(a__zeros)
      a__zeros -> cons(0,zeros)
      a__head(cons(X,L)) -> mark(X)
      a__tail(cons(X,L)) -> mark(L)
      mark(incr(X)) -> a__incr(mark(X))
      mark(adx(X)) -> a__adx(mark(X))
      mark(nats) -> a__nats
      mark(zeros) -> a__zeros
      mark(head(X)) -> a__head(mark(X))
      mark(tail(X)) -> a__tail(mark(X))
      mark(nil) -> nil
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      mark(s(X)) -> s(mark(X))
      mark(0) -> 0
      a__incr(X) -> incr(X)
      a__adx(X) -> adx(X)
      a__nats -> nats
      a__zeros -> zeros
      a__head(X) -> head(X)
      a__tail(X) -> tail(X)
      

   can be proved by using AProVE
2. The µ-termination of ExIntrod_GM01 is proved in [BLR02, Example 10] by using CSRPO.
3. The µ-termination of ExIntrod_GM01 can be proved by using a polynomial interpretation (computed by MuTerm):

       Proof of termination for ExIntrod_GM01:
   
       [incr](X) = X + 1
       [nil] = 0
       [cons](X1,X2) = X1 + 1/2.X2
       [s](X) = X
       [adx](X) = X + 3
       [nats] = 5
       [zeros] = 1
       [0] = 0
       [head](X) = X + 1
       [tail](X) = 2.X + 1
       

4. The µ-termination of ExIntrod_GM01 can also be proved by using CSDP(computed by MuTerm).